functor VcGenMain (S : VCGEN_MAIN_STRUCTS) : VCGEN_MAIN =
struct
  open S
  
  structure I = Ir  
  structure Vc = Vc
  
  structure Irvc2vc = Irvc2vc (structure Ir = I
                               structure Vc = Vc)
  structure VcGen = VcGen (structure Ir = I
                           structure Irvc2vc = Irvc2vc)
  structure PtrProof = PtrProof (structure Irvc2vc = Irvc2vc)                            
  
  fun top ir =
      let val strVcList = VcGen.top (I.pind2prop ir)
          val (strVcList1, optStrVcList) = Irvc2vc.top strVcList
          val _ = Vc.ppTop (strVcList1, 1)
          val _ = Vc.ppTop (optStrVcList, 2)
          
(*          val _ = PtrProof.top ir*)
      in  ()
      end
end
